package pl.edu.pw.elka.dzielins.revanalyzer;

import static edu.mit.csail.sdg.alloy4.A4Reporter.NOP;

import java.io.BufferedReader;
import java.io.BufferedWriter;
import java.io.File;
import java.io.FileInputStream;
import java.io.FileOutputStream;
import java.io.FileReader;
import java.io.FileWriter;
import java.io.IOException;
import java.io.OutputStream;
import java.nio.file.Files;
import java.util.ArrayList;
import java.util.HashSet;
import java.util.LinkedHashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.UUID;

import kodkod.ast.Formula;

import org.apache.commons.lang3.StringUtils;
import org.apache.log4j.Logger;

import edu.mit.csail.sdg.alloy4.A4Reporter;
import edu.mit.csail.sdg.alloy4.ConstList;
import edu.mit.csail.sdg.alloy4.Util;
import edu.mit.csail.sdg.alloy4compiler.ast.Attr;
import edu.mit.csail.sdg.alloy4compiler.ast.Command;
import edu.mit.csail.sdg.alloy4compiler.ast.Decl;
import edu.mit.csail.sdg.alloy4compiler.ast.Expr;
import edu.mit.csail.sdg.alloy4compiler.ast.ExprConstant;
import edu.mit.csail.sdg.alloy4compiler.ast.Func;
import edu.mit.csail.sdg.alloy4compiler.ast.Module;
import edu.mit.csail.sdg.alloy4compiler.ast.Sig;
import edu.mit.csail.sdg.alloy4compiler.parser.CompUtil;
import edu.mit.csail.sdg.alloy4compiler.translator.A4Options;
import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution;
import edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod;
import pl.edu.pw.elka.dzielins.revanalyzer.alloy.AlloyLogger;
import pl.edu.pw.elka.dzielins.revanalyzer.alloy.io.Reader;
import pl.edu.pw.elka.dzielins.revanalyzer.alloy.io.Writer;
import pl.edu.pw.elka.dzielins.revanalyzer.instance.Instance;
import pl.edu.pw.elka.dzielins.revanalyzer.instance.InstanceObject;
import pl.edu.pw.elka.dzielins.revanalyzer.instance.InstanceRelation;
import pl.edu.pw.elka.dzielins.revanalyzer.model.Model;
import pl.edu.pw.elka.dzielins.revanalyzer.model.ModelFact;
import pl.edu.pw.elka.dzielins.revanalyzer.model.ModelObject;
import pl.edu.pw.elka.dzielins.revanalyzer.model.ModelRelation;

public class Revanalyzer {
	private static final Logger LOG = Logger.getLogger(Revanalyzer.class);
	
	public A4Solution revanalyze(Model model, Instance instance) throws Exception {	
		File file = new File(UUID.randomUUID().toString());

		Writer writer = new Writer();
		writer.writeAlloy(instance, model, file);

		Module world = CompUtil.parseEverything_fromFile(new AlloyLogger(), null, file.getAbsolutePath());
		Command cmd = world.getAllCommands().get(0);
		A4Solution solution = TranslateAlloyToKodkod.execute_command(new AlloyLogger(), world.getAllReachableSigs(), cmd, new A4Options());	
		
		file.delete();
		
		return solution;
		
		/*A4Reporter reporter;
        List<Sig> sigs;
        Command command;
        A4Options options = new A4Options();
        
		try {
			// reporter
			reporter = new AlloyLogger();
			// command
			Expr run = (new Func(null, "emptyPred", null, null, ExprConstant.TRUE)).call();
			command = new Command(false, -1, -1, -1, run);			
			// sigs
			sigs = new ArrayList<Sig>();
			// from model
			for (ModelObject modelObject : model.getObjects()) {
				sigs.add(modelObject.getSig());
				Set<InstanceObject> set = instance.getInheritanceMap().get(modelObject);
				if (set != null) {
					//command = command.change(modelObject.getSig(), true, set.size());
				} else {
					//command = command.change(modelObject.getSig(), true, 0);
				}
			}
			// from instance
			for (InstanceObject instanceObject : instance.getObjects()) {
				sigs.add(instanceObject.getSig());
			}
			
			System.out.println(command.toString());
			
			// options
			options.solver = A4Options.SatSolver.SAT4J;

			// facts
			// from model
			for (ModelFact modelFact : model.getFacts()) {
				Sig.UNIV.addFact(modelFact.getExpression());
			}
			// from instance (relations)
			for (InstanceObject instanceObject : instance.getObjects()) {
				for (ModelRelation mr : instanceObject.getBaseObject().getAllRelations()) {
					Expr expr = null;
					if (instanceObject.getRelations().get(mr) == null || instanceObject.getRelations().get(mr).isEmpty()) {
						expr = instanceObject.getSig().join(mr.getField()).no();						
					} else {
						for (InstanceRelation relation : instanceObject.getRelations().get(mr)) {
							for (InstanceObject argument : relation.getArguments()) {
								if (expr == null)
									expr = argument.getSig();
								else
									expr = expr.plus(argument.getSig());	
							}
						}
						if (expr != null)
							//expr = expr.equal(instanceObject.getSig().join(mr.getField()));
							expr = instanceObject.getSig().join(mr.getField()).equal(expr);
					}					
					System.out.println(expr.toString());
					mr.getOwner().getSig().addFact(expr);
				}
			}
			// from instance (extensions)
			for (ModelObject modelObject : model.getObjects()) {
				Expr expr = null;
				// atoms
				for (InstanceObject io : instance.getInheritanceMap().get(modelObject)) {
					if (expr==null)
						expr = io.getSig();
					else
						expr = expr.plus(io.getSig());			
				}
				// subsigs
				for (ModelObject mo : model.getHiearchyMap().get(modelObject)) {
					if (expr==null)
						expr = mo.getSig();
					else
						expr = expr.plus(mo.getSig());
				}
				if (expr!=null) {
					//expr = CompUtil.parseOneExpression_fromString(model.getModule(), "Set = Set02 + Set01");
					expr = modelObject.getSig().equal(expr);
					System.out.println(expr.toString());
					Sig.UNIV.addFact(expr);
				}
			}
			
			System.out.println(sigs.toString());
			A4Solution solution;
			solution = TranslateAlloyToKodkod.execute_command(reporter, sigs, command, options);
			return solution;
		} catch (Exception e) {
			e.printStackTrace();
			return null;
		}*/
	}
}
